theory Memory_SEC
imports "../GPTEE_Instantiation" "TEEC_IPC_SEC"
begin
section "TEEC_integrity"
lemma TEEC_AllocateSharedMemory_integrity:
assumes p1: "a = hyperc (TEEC_ALLOCATESHAREDMEMORY ctx shm)"
shows "∀ d s s'. reachable0 s ∧ ((the (domain_of_event s a)) ∖↝ d) ∧ (s, s') ∈ exec_event a ⟶ (s ∼ d ∼ s')"
proof -
{
fix s s' d
assume a1: "reachable0 s"
assume a2: "((the (domain_of_event s a)) ∖↝ d)"
assume a3: "(s,s') ∈ exec_event a"
have a5: "s≠s'⟶((the (domain_of_event s a)) ∖↝ (TEE sysconf))"
by (metis a2 ins_no_intf_tee ins_tee_intf_all non_interference1_def)
have a4: "exec_event a = {(s,s'). s'∈{fst (TEEC_AllocateSharedMemory sysconf s ctx shm)}}"
using p1 exec_event_def by simp
have "(s ∼ d ∼ s')"
proof(cases "current s ≠ REE sysconf")
case True
then have "s=fst (TEEC_AllocateSharedMemory sysconf s ctx shm)"using TEEC_AllocateSharedMemory_def
by simp
then show ?thesis using vpeq1_def using a3 a4 by auto
next
case False
then have a6: "(the (domain_of_event s a)) = REE sysconf"
by simp
then show ?thesis
proof (cases "d = TEE sysconf")
case True
then have b1: "(s ∼ d ∼ s') = vpeq_TEE s d s'"
by simp
then have b2:"tee_memories (TEE_state s) = tee_memories (TEE_state s')"
proof(cases "(flags shm) ≠ TEEC_MEM_INPUT ∨ (flags shm) ≠ TEEC_MEM_OUTPUT")
case True
then have "s=fst (TEEC_AllocateSharedMemory sysconf s ctx shm)" using TEEC_AllocateSharedMemory_def
by simp
then show ?thesis
using a3 a4 by auto
next
case False
then show ?thesis
by simp
qed
then show ?thesis using b1 b2
by simp
next
case False
then have c1: "d ≠ TEE sysconf" by auto
then show ?thesis
proof (cases "d = REE sysconf")
case True
then show ?thesis
using a2 a6 nintf_neq by blast
next
case False
then have b4: "is_TA sysconf d"
using c1 is_TA_def by blast
then show ?thesis
proof - {
have b5: "(s ∼ d ∼ s') = vpeq_TA s d s'" using False b4 c1 vpeq1_def by presburger
have b6: "tee_memories (TEE_state s) = tee_memories (TEE_state s')"
proof (cases "(flags shm) ≠ TEEC_MEM_INPUT ∨ (flags shm) ≠ TEEC_MEM_OUTPUT")
case True
then have "s=fst (TEEC_AllocateSharedMemory sysconf s ctx shm)"
using TEEC_AllocateSharedMemory_def
by auto
then show ?thesis using a3 a4 by auto
next
case False
then show ?thesis
by auto
qed
then show ?thesis using b5
by simp
}
qed
qed
qed
qed
}
then show ?thesis
by blast
qed
lemma TEEC_AllocateSharedMemory_integrity_e:
"integrity_e (hyperc (TEEC_ALLOCATESHAREDMEMORY ctx shm))"
using TEEC_AllocateSharedMemory_integrity integrity_e_def
by fastforce
lemma TEEC_RegisterSharedMemory_integrity:
assumes p1: "a = hyperc (TEEC_REGISTERSHAREDMEMORY ctx shm)"
shows "∀ d s s'. reachable0 s ∧ ((the (domain_of_event s a)) ∖↝ d) ∧ (s, s') ∈ exec_event a ⟶ (s ∼ d ∼ s')"
proof - {
fix s s' d
assume a1: "reachable0 s"
assume a2: "((the (domain_of_event s a)) ∖↝ d)"
assume a3: "(s,s') ∈ exec_event a"
have a5: "s≠s'⟶((the (domain_of_event s a)) ∖↝ (TEE sysconf))"
by (metis a2 ins_no_intf_tee ins_tee_intf_all non_interference1_def)
have a4: "exec_event a = {(s,s'). s'∈{fst (TEEC_RegisterSharedMemory sysconf s ctx shm)}}"
using p1 exec_event_def by simp
have "(s ∼ d ∼ s')"
proof (cases "current s ≠ REE sysconf")
case True
then have "s=fst (TEEC_RegisterSharedMemory sysconf s ctx shm)"using TEEC_RegisterSharedMemory_def
by simp
then show ?thesis
using a3 a4 by auto
next
case False
then have a6: "(the (domain_of_event s a)) = REE sysconf" by simp
then show ?thesis
proof(cases "d = TEE sysconf")
case True
then have b1: "(s ∼ d ∼ s') = vpeq_TEE s d s'"
by simp
then have b2: "tee_memories (TEE_state s) = tee_memories (TEE_state s')"
proof(cases "(flags shm) ≠ TEEC_MEM_INPUT ∨ (flags shm) ≠ TEEC_MEM_OUTPUT")
case True
then have "s=fst (TEEC_RegisterSharedMemory sysconf s ctx shm)" using TEEC_RegisterSharedMemory_def
by auto
then show ?thesis
using a3 a4 by fastforce
next
case False
then show ?thesis
by simp
qed
then have b3: "ta_mgr (TEE_state s) =ta_mgr (TEE_state s')"
proof(cases "(flags shm) ≠ TEEC_MEM_INPUT ∨ (flags shm) ≠ TEEC_MEM_OUTPUT")
case True
then have "s=fst (TEEC_RegisterSharedMemory sysconf s ctx shm)" using TEEC_RegisterSharedMemory_def
by auto
then show ?thesis
using a3 a4 by fastforce
next
case False
then show ?thesis
by auto
qed
then show ?thesis using b1 b2 b3
by simp
next
case False
then have c1: "d ≠ TEE sysconf"
by simp
then show ?thesis
proof (cases "d = REE sysconf")
case True
then show ?thesis
using a2 a6 nintf_neq by blast
next
case False
then have b4: "is_TA sysconf d"
using c1 by auto
then show ?thesis
proof -{
have b5: "(s ∼ d ∼ s') = vpeq_TA s d s'" by (meson False b4 c1 vpeq1_def)
have b6: "tee_memories (TEE_state s) = tee_memories (TEE_state s')"
proof (cases "(flags shm) ≠ TEEC_MEM_INPUT ∨ (flags shm) ≠ TEEC_MEM_OUTPUT")
case True
then have "s=fst (TEEC_RegisterSharedMemory sysconf s ctx shm)" using TEEC_RegisterSharedMemory_def
by auto
then show ?thesis
using a3 a4 by auto
next
case False
then show ?thesis
by simp
qed
then show ?thesis using b5
by simp
}
qed
qed
qed
qed
}
then show ?thesis
by blast
qed
lemma TEEC_RegisterSharedMemory_integrity_e:
"integrity_e (hyperc (TEEC_REGISTERSHAREDMEMORY ctx shm))"
using TEEC_RegisterSharedMemory_integrity integrity_e_def
by fastforce
lemma TEEC_ReleaseSharedMemory_integrity:
assumes p1: "a = hyperc (TEEC_RELEASESHAREDMEMORY shm)"
shows "∀ d s s'. reachable0 s ∧ ((the (domain_of_event s a)) ∖↝ d) ∧ (s, s') ∈ exec_event a ⟶ (s ∼ d ∼ s')"
proof - {
fix s s' d
assume a1: "reachable0 s"
assume a2: "((the (domain_of_event s a)) ∖↝ d)"
assume a3: "(s,s') ∈ exec_event a"
have a5: "s≠s'⟶((the (domain_of_event s a)) ∖↝ (TEE sysconf))"
by (metis a2 ins_no_intf_tee ins_tee_intf_all non_interference1_def)
have a4: "exec_event a = {(s,s'). s'∈{(TEEC_ReleaseSharedMemory sysconf s shm)}}"
using p1 exec_event_def by simp
have "(s ∼ d ∼ s')"
proof (cases "current s ≠ REE sysconf")
case True
then have "s = (TEEC_ReleaseSharedMemory sysconf s shm)" using TEEC_ReleaseSharedMemory_def
by simp
then show ?thesis using a3 a4
by auto
next
case False
then have a6: "(the (domain_of_event s a)) = REE sysconf" by simp
then show ?thesis
proof (cases "d = TEE sysconf")
case True
then have b1: "(s ∼ d ∼ s') = vpeq_TEE s d s'" by simp
then have b2: "tee_memories(TEE_state s) = tee_memories(TEE_state s')"
proof (cases "shared_id shm = 0")
case True
then have "s = (TEEC_ReleaseSharedMemory sysconf s shm)" using TEEC_ReleaseSharedMemory_def
by simp
then show ?thesis using a3 a4
by simp
next
case False
then have "TEE_state s = TEE_state (TEEC_ReleaseSharedMemory sysconf s shm)"
using TEEC_ReleaseSharedMemory_def
by simp
then show ?thesis using TEE_TYPE.defs using a3 a4
by simp
qed
then show ?thesis using b1 b2
by simp
next
case False
then have c1: "d ≠ TEE sysconf"
by simp
then show ?thesis
proof (cases "d = REE sysconf")
case True
then show ?thesis
using a2 a6 nintf_neq by blast
next
case False
then have b3: "is_TA sysconf d"
using c1 by auto
then show ?thesis
proof - {
have b4: "(s ∼ d ∼ s') = vpeq_TA s d s'"
using False b3 c1 vpeq1_def by presburger
have b5: "tee_memories (TEE_state s) = tee_memories (TEE_state s')"
proof (cases "shared_id shm = 0")
case True
then have "s = (TEEC_ReleaseSharedMemory sysconf s shm)" using TEEC_ReleaseSharedMemory_def
by simp
then show ?thesis using a3 a4
by simp
next
case False
then have "TEE_state s = TEE_state (TEEC_ReleaseSharedMemory sysconf s shm)"
using TEEC_ReleaseSharedMemory_def
by simp
then show ?thesis using a3 a4
by simp
qed
then show ?thesis using b4
by simp
}
qed
qed
qed
qed
}
then show ?thesis
by blast
qed
lemma TEEC_ReleaseSharedMemory_integrity_e:
"integrity_e (hyperc (TEEC_RELEASESHAREDMEMORY shm))"
using TEEC_ReleaseSharedMemory_integrity integrity_e_def
by fastforce
section "TEE_integrity"
lemma TEE_CheckMemoryAccessRights_integrity:
assumes p1: "a = hyperc (TEE_CHECKMEMORYACCESSRIGHTS aF memblock buffer_size)"
shows "∀ d s s'. reachable0 s ∧ ((the (domain_of_event s a)) ∖↝ d) ∧ (s, s') ∈ exec_event a ⟶ (s ∼ d ∼ s')"
proof - {
fix s s' d
assume a1: "reachable0 s"
assume a2: "((the (domain_of_event s a)) ∖↝ d)"
assume a3: "(s,s') ∈ exec_event a"
have a5: "s≠s'⟶((the (domain_of_event s a)) ∖↝ (TEE sysconf))"
by (metis a2 ins_no_intf_tee ins_tee_intf_all non_interference1_def)
have a4: "exec_event a = {(s,s'). s'∈{(s)}}"
using p1 exec_event_def by simp
have "(s ∼ d ∼ s')"
using a3 a4 by auto
}
then show ?thesis
by blast
qed
lemma TEE_CheckMemoryAccessRights_integrity_e:
"integrity_e (hyperc (TEE_CHECKMEMORYACCESSRIGHTS aF memblock buffer_size))"
using TEE_CheckMemoryAccessRights_integrity integrity_e_def
by fastforce
lemma TEE_Malloc_integrity:
assumes p1: "a = hyperc (TEE_MALLOC buffer_size h)"
shows "∀ d s s'. reachable0 s ∧ ((the (domain_of_event s a)) ∖↝ d) ∧ (s, s') ∈ exec_event a ⟶ (s ∼ d ∼ s')"
proof -{
fix s s' d
assume a1: "reachable0 s"
assume a2: "((the (domain_of_event s a)) ∖↝ d)"
assume a3: "(s,s') ∈ exec_event a"
have a5: "s≠s'⟶((the (domain_of_event s a)) ∖↝ (TEE sysconf))"
by (metis a2 ins_no_intf_tee ins_tee_intf_all non_interference1_def)
have a4: "exec_event a = {(s,s'). s'∈{(TEE_Malloc sysconf s buffer_size h)}}"
using p1 exec_event_def by simp
have b: "s' = (TEE_Malloc sysconf s buffer_size h)" using p1 a3 a4
by blast
have "(s ∼ d ∼ s')"
proof (cases "current s = TEE sysconf ∨ current s = REE sysconf")
case True
then have "s = (TEE_Malloc sysconf s buffer_size h)" using TEE_Malloc_def
by simp
then show ?thesis using a3 a4
by auto
next
case False
then have a6: "¬(current s = TEE sysconf ∨ current s = REE sysconf)"
by auto
then show ?thesis
proof (cases "(exec_prime s) ≠ []")
case True
then have "s' = s" using TEE_Malloc_def b a6
by simp
then show ?thesis
by auto
next
case False
then have exec: "¬((exec_prime s) ≠ [])"
by simp
then show ?thesis
proof (cases "((h ≠ TEE_MALLOC_FILL_ZERO) ∧ (h ≠ TEE_USER_MEM_HINT_NO_FILL_ZERO))")
case True
then have "s' = s" using a6 exec b TEE_Malloc_def
by simp
then show ?thesis
by auto
next
case False
then have noth: "¬((h ≠ TEE_MALLOC_FILL_ZERO) ∧ (h ≠ TEE_USER_MEM_HINT_NO_FILL_ZERO))"
by simp
then show ?thesis
proof (cases "d = TEE sysconf")
case True
let ?newTEESize = "tee_total_size(TEE_state s) - buffer_size"
let ?newblk = "mem_alloc s buffer_size"
let ?lst = "?newblk # tee_memories(TEE_state s)"
let ?newBIDpointer = "BIDpointer(ta_mgr(TEE_state s)) + 1"
have not0: "block_id ?newblk ≠ 0" using newBlockID3_not_zero mem_alloc_def
by simp
have ss': "s' = s⦇TEE_state := (TEE_state s)⦇tee_total_size := ?newTEESize, tee_memories := ?lst,
tee_memories := ?lst, ta_mgr:=ta_mgr(TEE_state s)⦇BIDpointer:=?newBIDpointer⦈⦈⦈"
using TEE_Malloc_def a6 exec noth b by auto
have "{x. x∈set(tee_memories (TEE_state s))∧ (block_id x=0)} =
{x. x∈set(tee_memories (TEE_state s'))∧ (block_id x=0)}"
using ss' not0
by auto
then show ?thesis using vpeq1_def vpeq_TEE_def True
by auto
next
case False
then have g: "¬(d = TEE sysconf)" using False
by auto
then show ?thesis
proof (cases "d = REE sysconf")
case True
have "ree_total_size(REE_state s) = ree_total_size (REE_state s')
∧driver_mem(REE_state s) = driver_mem(REE_state s')"
using TEE_Malloc_def b
by simp
then show ?thesis using False True
by simp
next
case False
then have gg: "¬(d = REE sysconf)"using False
by blast
then show ?thesis
proof (cases "is_TA sysconf d")
case True
then show ?thesis
proof (cases "current s = d")
case True
then have "((the (domain_of_event s a)) ↝ d)"
by auto
then show ?thesis using a2
by simp
next
case False
let ?newTEESize = "tee_total_size(TEE_state s) - buffer_size"
let ?newblk = "mem_alloc s buffer_size"
let ?lst = "?newblk # tee_memories(TEE_state s)"
let ?newBIDpointer = "BIDpointer(ta_mgr(TEE_state s)) + 1"
have "current s ≠ d" using False
by blast
then have os:"ownership ?newblk ≠ d" using mem_alloc_def
by simp
have "s' = s⦇TEE_state := (TEE_state s)⦇tee_total_size := ?newTEESize, tee_memories := ?lst, tee_memories := ?lst,
ta_mgr:=ta_mgr(TEE_state s)⦇BIDpointer:=?newBIDpointer⦈⦈⦈"
using TEE_Malloc_def a6 exec noth b by auto
then have "{x. x∈set(tee_memories (TEE_state s))∧ (ownership x=d)} =
{x. x∈set(tee_memories (TEE_state s'))∧ (ownership x=d)}"
using os
by auto
then show ?thesis using vpeq1_def vpeq_TA_def True
by auto
qed
next
case False
then have ggg: "¬(is_TA sysconf d)" using False
by blast
show ?thesis using g gg ggg
by auto
qed
qed
qed
qed
qed
qed
}
then show ?thesis
by blast
qed
lemma TEE_Malloc_integrity_e:
"integrity_e (hyperc (TEE_MALLOC buffer_size h))"
using TEE_Malloc_integrity integrity_e_def
by fastforce
lemma TEE_Realloc_integrity:
assumes p1: "a = hyperc (TEE_REALLOC memblock new_size)"
shows "∀ d s s'. reachable0 s ∧ ((the (domain_of_event s a)) ∖↝ d) ∧ (s, s') ∈ exec_event a ⟶ (s ∼ d ∼ s')"
proof -{
fix s s' d
assume a1: "reachable0 s"
assume a2: "((the (domain_of_event s a)) ∖↝ d)"
assume a3: "(s,s') ∈ exec_event a"
have a5: "s≠s'⟶((the (domain_of_event s a)) ∖↝ (TEE sysconf))"
by (metis a2 ins_no_intf_tee ins_tee_intf_all non_interference1_def)
have a4: "exec_event a = {(s,s'). s'∈{(TEE_Realloc sysconf s memblock new_size)}}"
using p1 exec_event_def by simp
have b: "s' = (TEE_Realloc sysconf s memblock new_size)" using p1 a3 a4
by blast
have "(s ∼ d ∼ s')"
proof (cases "current s = TEE sysconf ∨ current s = REE sysconf")
case True
then have "s = TEE_Realloc sysconf s memblock new_size" using TEE_Realloc_def
by simp
then show ?thesis using a3 a4
by auto
next
case False
then have a6: "¬(current s = TEE sysconf ∨ current s = REE sysconf)"
by auto
then show ?thesis
proof (cases "(exec_prime s) ≠ []")
case True
then have "s' = s" using TEE_Realloc_def a6 b
by simp
then show ?thesis
by auto
next
case False
then have exec: "¬((exec_prime s) ≠ [])"
by simp
then show ?thesis
proof (cases "d = TEE sysconf")
case True
have b1: "(s ∼ d ∼ s') = vpeq_TEE s d s'" using True by simp
have b2: "tee_memories(TEE_state s) = tee_memories(TEE_state s')" using TEE_Realloc_def a6 exec b
by simp
then show ?thesis using vpeq1_def vpeq_TEE_def True
by presburger
next
case False
then have g: "¬(d = TEE sysconf)"
by simp
then show ?thesis
proof (cases "d = REE sysconf")
case True
then have "ree_total_size(REE_state s) = ree_total_size (REE_state s')
∧driver_mem(REE_state s) = driver_mem(REE_state s')"
using b TEE_Realloc_def
by auto
then show ?thesis using vpeq1_def vpeq_REE_def b g True
by auto
next
case False
then have gg: "¬(d = REE sysconf)"
by simp
then show ?thesis
proof (cases "is_TA sysconf d")
case True
let ?newTEESize = "tee_total_size(TEE_state s) - new_size + (size memblock)"
have "s' = s⦇TEE_state := (TEE_state s)⦇tee_total_size := ?newTEESize⦈⦈"
using TEE_Realloc_def a6 exec b
by simp
then show ?thesis
by auto
next
case False
then have ggg: "¬(is_TA sysconf d)"
by blast
then show ?thesis using g gg ggg
by simp
qed
qed
qed
qed
qed
}
then show ?thesis
by blast
qed
lemma TEE_Realloc_integrity_e:
"integrity_e (hyperc (TEE_REALLOC memblock new_size))"
using TEE_Realloc_integrity integrity_e_def
by fastforce
lemma q1:" newIdFromList lst∉set lst"
proof -
{
have a1:"(SOME a. (a≥(2::nat))∧a∉set lst)∉set lst" using some_eq_imp newIDexist newIdFromList_def
by (metis (mono_tags, lifting))
show ?thesis using a1 newIdFromList_def by simp
}qed
lemma q2:"y∈(set lst)∧x=newIdFromList lst⟶x≠y"
proof -
{
assume a1:"x=newIdFromList lst"
assume a2:"y∈(set lst)"
have a3:"x∉set lst" using q1 a1 by blast
have a4:"x≠y" using a3 a2 by blast
}
then show ?thesis by blast
qed
lemma q3:"∀x y lst. y∈(set lst)∧x=newIdFromList lst⟶x≠y"
using q2 by simp
axiomatization where test:"∀x y. reachable0 s ∧ x∈set(tee_memories(TEE_state s)) ∧ y∈set(tee_memories(TEE_state s)) ∧ x ≠ y ⟶ block_id x ≠ block_id y"
lemma TEE_Free_integrity:
assumes p1: "a = hyperc (TEE_FREE memblock)"
shows "∀ d s s'. reachable0 s ∧ ((the (domain_of_event s a)) ∖↝ d) ∧ (s, s') ∈ exec_event a ⟶ (s ∼ d ∼ s')"
proof -{
fix s s' d
assume a1: "reachable0 s"
assume a2: "((the (domain_of_event s a)) ∖↝ d)"
assume a3: "(s,s') ∈ exec_event a"
have a4: "exec_event a = {(s,s'). s'∈{(TEE_Free sysconf s memblock)}}"
using p1 exec_event_def by simp
have b: "s' = (TEE_Free sysconf s memblock)" using p1 a3 a4
by blast
have "(s ∼ d ∼ s')"
proof (cases "current s = TEE sysconf ∨ current s = REE sysconf")
case True
then have "s = (TEE_Free sysconf s memblock)" using TEE_Free_def
by simp
then show ?thesis using a3 a4
by auto
next
case False
then have a11: "¬(current s = TEE sysconf ∨ current s = REE sysconf)"
by simp
then have a6: "is_TA sysconf (the (domain_of_event s a))"
by auto
then show ?thesis
proof (cases "(exec_prime s) ≠ []
∨ ownership memblock ≠ current s
∨ memblock ∉ set(filter (λx.(ownership x) = (ownership memblock)) (tee_memories(TEE_state s)))
∨ block_id memblock < 2")
case True
then have "s' = s" using TEE_Free_def a6 b
by metis
then show ?thesis
by auto
next
case False
then have exec: "¬((exec_prime s) ≠ [] ∨ ownership memblock ≠ current s)"
by blast
have owner: "ownership memblock = current s" using False
by blast
have i0: "memblock ∈ set(filter (λx.(ownership x) = (ownership memblock)) (tee_memories(TEE_state s)))" using False
by blast
then have i: "memblock ∈ set(tee_memories(TEE_state s))"
by simp
have id2: "¬(block_id memblock < 2)" using False
by blast
let ?newTEESize = "tee_total_size(TEE_state s) + (size memblock)"
let ?newlst = "filter (λx.(block_id x) ≠ (block_id memblock)) (tee_memories(TEE_state s))"
have ss': "s' = s⦇TEE_state := (TEE_state s)⦇tee_total_size := ?newTEESize, tee_memories := ?newlst⦈⦈"
using TEE_Free_def a6 exec b i0 id2
by simp
have not0: "block_id memblock ≠ 0" using id2
by simp
then show ?thesis
proof (cases "d = TEE sysconf")
case True
have "{x. x∈set(tee_memories (TEE_state s))∧ (block_id x=0)} =
{x. x∈set(tee_memories (TEE_state s'))∧ (block_id x=0)}"
using TEE_Free_def b a6 exec ss' not0
by force
then show ?thesis using vpeq_TEE_def vpeq1_def True
by auto
next
case False
then have g: "¬(d = TEE sysconf)"
by simp
then show ?thesis
proof (cases "d = REE sysconf")
case True
then show ?thesis using b ss' vpeq_REE_def vpeq1_def g
by fastforce
next
case False
then have gg: "¬(d = REE sysconf)"
by blast
then show ?thesis
proof (cases "is_TA sysconf d")
case True
then show ?thesis
proof (cases "current s = d")
case True
then have "((the (domain_of_event s a)) ↝ d)"
by auto
then show ?thesis using a2
by auto
next
case False
then have c:"current s ≠ d"
by blast
have c1: "∀x∈set(tee_memories (TEE_state s)). x ≠ memblock ⟶ block_id memblock ≠ block_id x" using test i a1
by blast
have "{x. x∈set(tee_memories (TEE_state s)) ∧ (ownership x=d)} =
{x. x∈set(?newlst) ∧ (ownership x=d)}"
using owner c c1
by force
then show ?thesis using ss' vpeq_TA_def vpeq1_def g gg True
by auto
qed
next
case False
then have ggg: "¬(is_TA sysconf d)"
by blast
then show ?thesis using g gg ggg
by simp
qed
qed
qed
qed
qed
}
then show ?thesis
by blast
qed
lemma TEE_Free_integrity_e:
"integrity_e (hyperc (TEE_FREE memblock))"
using TEE_Free_integrity integrity_e_def
by fastforce
section "TEEC_Confidentiality"
lemma TEEC_AllocateSharedMemory_weak_confidentiality:
assumes p1: "a = hyperc (TEEC_ALLOCATESHAREDMEMORY ctx shm)"
shows "∀ d s t.
reachable0 s ∧
reachable0 t ∧
(s ∼ d ∼ t) ∧
((domain_of_event s a) = (domain_of_event t a)) ∧
(get_exec_prime s=get_exec_prime t)∧
((the (domain_of_event s a)) ↝ d) ∧
(s ∼ (the (domain_of_event s a)) ∼ t) ⟶
(∀ s' t'. (s, s') ∈ exec_event a ∧ (t, t') ∈ exec_event a ⟶ (s' ∼ d ∼ t'))"
proof -
{
fix s t d s' t'
assume a1:"reachable0 s"
assume a2:"reachable0 t"
assume a3:"s∼d∼t"
assume a31:"exec_prime s=exec_prime t"
assume a4:"(domain_of_event s a) = (domain_of_event t a)"
assume a5:"(the (domain_of_event s a)) ↝ d"
assume a6:"s ∼ (the (domain_of_event s a)) ∼ t"
assume a7:"(s, s') ∈ exec_event a"
assume a8:"(t, t') ∈ exec_event a"
have "s'∼d∼t'"
proof -{
have b1: "s' = fst (TEEC_AllocateSharedMemory sysconf s ctx shm)" using exec_event_def p1 a7
by simp
have b2: "t' = fst (TEEC_AllocateSharedMemory sysconf t ctx shm)" using exec_event_def p1 a8
by simp
have b3: "current s = current t" using domain_of_event_def a4
by simp
show ?thesis
proof (cases "current s ≠ REE sysconf")
case True
then show ?thesis using TEEC_AllocateSharedMemory_def b1 b2 b3 a3
by fastforce
next
case False
have c1: "current s = REE sysconf"
using False by blast
then show ?thesis
proof (cases "(exec_prime s) ≠ []")
case True
then show ?thesis using TEEC_AllocateSharedMemory_def b1 b2 b3 a3
by fastforce
next
case False
then show ?thesis
proof (cases "d = REE sysconf")
case True
have d1: "vpeq_REE s d t"using a3 vpeq1_def
using True tee_no_ree by auto
have d2: "ree_total_size(REE_state s) = ree_total_size (REE_state t)" using d1
by simp
have d3: "driver_mem(REE_state s) = driver_mem (REE_state t)" using d1
by simp
have d4: "ree_total_size(REE_state s') = ree_total_size(REE_state t')" using TEEC_AllocateSharedMemory_def b1 b2 d2
by simp
have d5: "driver_mem(REE_state s') = driver_mem(REE_state t')" using TEEC_AllocateSharedMemory_def b1 b2 d3
by simp
then show ?thesis using d4 d5
using True tee_no_ree vpeq1_def vpeq_REE_def by presburger
next
case False
have ggg: "d ≠ REE sysconf" using False
by simp
then show ?thesis
proof (cases "is_TA sysconf d")
case True
then have e: "is_TA sysconf d" using True
by simp
then have "vpeq_TA s d t" using True a3 vpeq1_def
by simp
then have e1: " {x. x∈set(tee_memories (TEE_state s))∧ (ownership x=d)} =
{x. x∈set(tee_memories (TEE_state t))∧ (ownership x=d)}"
by simp
then have e2: "TEE_state s = TEE_state s'" using b1 a7 TEEC_AllocateSharedMemory_def
by simp
then have e3: "TEE_state t = TEE_state t'" using b2 a8 TEEC_AllocateSharedMemory_def
by simp
then have e4: " {x. x∈set(tee_memories (TEE_state s'))∧ (ownership x=d)} =
{x. x∈set(tee_memories (TEE_state t'))∧ (ownership x=d)}" using e1 e2 e3
by simp
then show ?thesis
using True e4 by fastforce
next
case False
have gg: "¬(is_TA sysconf d)" using False
by simp
then show ?thesis
proof (cases "d = TEE sysconf")
case True
have f: "vpeq_TEE s d t"using a3 vpeq1_def
using True by auto
then have f1: "{x. x∈set(tee_memories (TEE_state s))∧ (block_id x=0)} =
{x. x∈set(tee_memories (TEE_state t))∧ (block_id x=0)}" using f
by simp
then have f3: "TEE_state s = TEE_state s'" using TEEC_AllocateSharedMemory_def b1
by simp
then have f31: "{x. x∈set(tee_memories (TEE_state s))∧ (block_id x=0)} =
{x. x∈set(tee_memories (TEE_state s'))∧ (block_id x=0)}" using f3
by simp
then have f4: "TEE_state t = TEE_state t'" using TEEC_AllocateSharedMemory_def b2
by simp
then have f41: "{x. x∈set(tee_memories (TEE_state t))∧ (block_id x=0)} =
{x. x∈set(tee_memories (TEE_state t'))∧ (block_id x=0)}" using f4
by simp
then have f5: "{x. x∈set(tee_memories (TEE_state s'))∧ (block_id x=0)} =
{x. x∈set(tee_memories (TEE_state t'))∧ (block_id x=0)}" using f1 f31 f41
by simp
then show ?thesis using f5
using True by auto
next
case False
then show ?thesis using vpeq1_def b1 b2 gg ggg
by simp
qed
qed
qed
qed
qed
}
qed
}
then show ?thesis
using get_exec_prime_def
by (smt (verit, best) Pair_inject)
qed
lemma TEEC_AllocateSharedMemory_weak_confidentiality_e:
"weak_confidentiality_e (hyperc (TEEC_ALLOCATESHAREDMEMORY ctx shm))"
using TEEC_AllocateSharedMemory_weak_confidentiality weak_confidentiality_e_def
by (smt (verit, del_insts) get_exec_prime_def)
lemma TEEC_RegisterSharedMemory_weak_confidentiality:
assumes p1: "a = hyperc (TEEC_REGISTERSHAREDMEMORY ctx shm)"
shows "∀ d s t.
reachable0 s ∧
reachable0 t ∧
(s ∼ d ∼ t) ∧
((domain_of_event s a) = (domain_of_event t a)) ∧
(get_exec_prime s=get_exec_prime t)∧
((the (domain_of_event s a)) ↝ d) ∧
(s ∼ (the (domain_of_event s a)) ∼ t) ⟶
(∀ s' t'. (s, s') ∈ exec_event a ∧ (t, t') ∈ exec_event a ⟶ (s' ∼ d ∼ t'))"
proof -
{
fix s t d s' t'
assume a1:"reachable0 s"
assume a2:"reachable0 t"
assume a3:"s∼d∼t"
assume a31:"exec_prime s=exec_prime t"
assume a4:"(domain_of_event s a) = (domain_of_event t a)"
assume a5:"(the (domain_of_event s a)) ↝ d"
assume a6:"s ∼ (the (domain_of_event s a)) ∼ t"
assume a7:"(s, s') ∈ exec_event a"
assume a8:"(t, t') ∈ exec_event a"
have "s'∼d∼t'"
proof -{
have b1: "s' = fst (TEEC_RegisterSharedMemory sysconf s ctx shm)" using exec_event_def p1 a7
by simp
have b2: "t' = fst (TEEC_RegisterSharedMemory sysconf t ctx shm)" using exec_event_def p1 a8
by simp
have b3: "current s = current t" using domain_of_event_def a4
by simp
show ?thesis
proof (cases "current s ≠ REE sysconf")
case True
then show ?thesis using TEEC_RegisterSharedMemory_def b1 b2 b3 a3
by fastforce
next
case False
have c1: "current s = REE sysconf"
using False by blast
then show ?thesis
proof (cases "(exec_prime s) ≠ []")
case True
then show ?thesis using TEEC_RegisterSharedMemory_def b1 b2 b3 a3
by fastforce
next
case False
then show ?thesis
proof (cases "d = REE sysconf")
case True
have d1: "vpeq_REE s d t"using a3 vpeq1_def
using True tee_no_ree by auto
have d2: "ree_total_size(REE_state s) = ree_total_size (REE_state t)" using d1
by simp
have d3: "driver_mem(REE_state s) = driver_mem (REE_state t)" using d1
by simp
have d4: "ree_total_size(REE_state s') = ree_total_size(REE_state t')" using TEEC_RegisterSharedMemory_def b1 b2 d2
by simp
have d5: "driver_mem(REE_state s') = driver_mem(REE_state t')" using TEEC_RegisterSharedMemory_def b1 b2 d3
by simp
then show ?thesis using d4 d5
using True tee_no_ree vpeq1_def vpeq_REE_def by presburger
next
case False
have ggg: "d ≠ REE sysconf" using False
by simp
then show ?thesis
proof (cases "is_TA sysconf d")
case True
then have e: "is_TA sysconf d" using True
by simp
then have "vpeq_TA s d t" using True a3 vpeq1_def
by simp
then have e1: " {x. x∈set(tee_memories (TEE_state s))∧ (ownership x=d)} =
{x. x∈set(tee_memories (TEE_state t))∧ (ownership x=d)}"
by simp
then have e2: "TEE_state s = TEE_state s'" using b1 a7 TEEC_RegisterSharedMemory_def
by simp
then have e3: "TEE_state t = TEE_state t'" using b2 a8 TEEC_RegisterSharedMemory_def
by simp
then have e4: " {x. x∈set(tee_memories (TEE_state s'))∧ (ownership x=d)} =
{x. x∈set(tee_memories (TEE_state t'))∧ (ownership x=d)}" using e1 e2 e3
by simp
then show ?thesis
using True e4 by fastforce
next
case False
have gg: "¬(is_TA sysconf d)" using False
by simp
then show ?thesis
proof (cases "d = TEE sysconf")
case True
have f: "vpeq_TEE s d t"using a3 vpeq1_def
using True by auto
then have f1: "{x. x∈set(tee_memories (TEE_state s))∧ (block_id x=0)} =
{x. x∈set(tee_memories (TEE_state t))∧ (block_id x=0)}" using f
by simp
then have f3: "TEE_state s = TEE_state s'" using TEEC_RegisterSharedMemory_def b1
by simp
then have f31: "{x. x∈set(tee_memories (TEE_state s))∧ (block_id x=0)} =
{x. x∈set(tee_memories (TEE_state s'))∧ (block_id x=0)}" using f3
by simp
then have f4: "TEE_state t = TEE_state t'" using TEEC_RegisterSharedMemory_def b2
by simp
then have f41: "{x. x∈set(tee_memories (TEE_state t))∧ (block_id x=0)} =
{x. x∈set(tee_memories (TEE_state t'))∧ (block_id x=0)}" using f4
by simp
then have f5: "{x. x∈set(tee_memories (TEE_state s'))∧ (block_id x=0)} =
{x. x∈set(tee_memories (TEE_state t'))∧ (block_id x=0)}" using f1 f31 f41
by simp
then show ?thesis using f5
using True by auto
next
case False
then show ?thesis using vpeq1_def b1 b2 gg ggg
by simp
qed
qed
qed
qed
qed
}
qed
}
then show ?thesis
using get_exec_prime_def
by (smt (verit, best) Pair_inject)
qed
lemma TEEC_RegisterSharedMemory_weak_confidentiality_e:
"weak_confidentiality_e (hyperc (TEEC_REGISTERSHAREDMEMORY ctx shm))"
using TEEC_RegisterSharedMemory_weak_confidentiality weak_confidentiality_e_def
by (smt (verit, del_insts) get_exec_prime_def)
lemma TEEC_ReleaseSharedMemory_weak_confidentiality:
assumes p1: "a = hyperc (TEEC_RELEASESHAREDMEMORY shm)"
shows "∀ d s t.
reachable0 s ∧
reachable0 t ∧
(s ∼ d ∼ t) ∧
((domain_of_event s a) = (domain_of_event t a)) ∧
(get_exec_prime s=get_exec_prime t)∧
((the (domain_of_event s a)) ↝ d) ∧
(s ∼ (the (domain_of_event s a)) ∼ t) ⟶
(∀ s' t'. (s, s') ∈ exec_event a ∧ (t, t') ∈ exec_event a ⟶ (s' ∼ d ∼ t'))"
proof -{
fix s t d s' t'
assume a1:"reachable0 s"
assume a2:"reachable0 t"
assume a3:"s∼d∼t"
assume a31:"exec_prime s=exec_prime t"
assume a4:"(domain_of_event s a) = (domain_of_event t a)"
assume a5:"(the (domain_of_event s a)) ↝ d"
assume a6:"s ∼ (the (domain_of_event s a)) ∼ t"
assume a7:"(s, s') ∈ exec_event a"
assume a8:"(t, t') ∈ exec_event a"
have "s'∼d∼t'"
proof -{
have b1: "s' = (TEEC_ReleaseSharedMemory sysconf s shm)" using exec_event_def p1 a7
by simp
have b2: "t' = (TEEC_ReleaseSharedMemory sysconf t shm)" using exec_event_def p1 a8
by simp
have b3: "current s = current t" using domain_of_event_def a4
by simp
show ?thesis
proof (cases "current s ≠ REE sysconf")
case True
then show ?thesis using TEEC_ReleaseSharedMemory_def b1 b2 b3 a3
by fastforce
next
case False
then have currents:"current s = REE sysconf" using False
by simp
show ?thesis
proof (cases "(exec_prime s) ≠ []")
case True
then show ?thesis using TEEC_ReleaseSharedMemory_def b1 b2 b3 a3
by (metis a31)
next
case False
then have exec: "¬((exec_prime s) ≠ [])"
by simp
then show ?thesis
proof (cases "shared_id shm = 0")
case True
then show ?thesis using TEEC_ReleaseSharedMemory_def b1 b2 b3 a3
by metis
next
case False
then have shid: "¬(shared_id shm = 0)"
by simp
then show ?thesis
proof (cases "d = REE sysconf")
case True
have c1: "vpeq_REE s d t"using a3 vpeq1_def
using True tee_no_ree by auto
have c2: "ree_total_size(REE_state s) = ree_total_size (REE_state t)" using c1
by simp
have c3: "driver_mem(REE_state s) = driver_mem (REE_state t)" using c1
by simp
let ?newREESize = "ree_total_size(REE_state s) + (alloced_size shm)"
let ?newlst = "filter (λ(x::MemBlock). (block_id x) ≠ (buffer shm)) (driver_mem(REE_state s))"
let ?newREESize_t = "ree_total_size(REE_state t) + (alloced_size shm)"
let ?newlst_t = "filter (λ(x::MemBlock). (block_id x) ≠ (buffer shm)) (driver_mem(REE_state t))"
have ss': "s' = s⦇REE_state := (REE_state s)⦇ree_total_size := ?newREESize, driver_mem := ?newlst⦈⦈"
using TEEC_ReleaseSharedMemory_def currents exec shid b1
by simp
have tt': "t' = t⦇REE_state := (REE_state t)⦇ree_total_size := ?newREESize_t, driver_mem := ?newlst_t⦈⦈"
using TEEC_ReleaseSharedMemory_def currents exec shid b2 b3 a31
by simp
have sizechange: "?newREESize = ?newREESize_t" using c2
by simp
have lstchange: "?newlst = ?newlst_t" using c3
by simp
have c4: "ree_total_size(REE_state s') = ree_total_size(REE_state t')"
using ss' tt' sizechange
by simp
have c5: "driver_mem(REE_state s') = driver_mem(REE_state t')"
using ss' tt' lstchange
by simp
then show ?thesis using c4 c5
using True tee_no_ree vpeq1_def vpeq_REE_def by presburger
next
case False
then have g: "d ≠ REE sysconf"
by simp
then have "(the (domain_of_event s a)) ∖↝ d" using interference1_def non_interference1_def currents
by (metis domain_of_event_def is_TEE_def option.sel tee_no_ree)
then show ?thesis using a5
by simp
qed
qed
qed
qed
}
qed
}
then show ?thesis
using get_exec_prime_def
by (smt (verit, best) Pair_inject)
qed
lemma TEEC_ReleaseSharedMemory_weak_confidentiality_e:
"weak_confidentiality_e (hyperc (TEEC_RELEASESHAREDMEMORY shm))"
using TEEC_ReleaseSharedMemory_weak_confidentiality weak_confidentiality_e_def
by (smt (verit, del_insts) get_exec_prime_def)
section "TEE_Confidentiality"
lemma TEE_CheckMemoryAccessRights_weak_confidentiality:
assumes p1: "a = hyperc (TEE_CHECKMEMORYACCESSRIGHTS aF memblock buffer_size)"
shows "∀ d s t.
reachable0 s ∧
reachable0 t ∧
(s ∼ d ∼ t) ∧
((domain_of_event s a) = (domain_of_event t a)) ∧
(get_exec_prime s=get_exec_prime t)∧
((the (domain_of_event s a)) ↝ d) ∧
(s ∼ (the (domain_of_event s a)) ∼ t) ⟶
(∀ s' t'. (s, s') ∈ exec_event a ∧ (t, t') ∈ exec_event a ⟶ (s' ∼ d ∼ t'))"
proof -{
fix s t d s' t'
assume a1:"reachable0 s"
assume a2:"reachable0 t"
assume a3:"s∼d∼t"
assume a31:"exec_prime s=exec_prime t"
assume a4:"(domain_of_event s a) = (domain_of_event t a)"
assume a5:"(the (domain_of_event s a)) ↝ d"
assume a6:"s ∼ (the (domain_of_event s a)) ∼ t"
assume a7:"(s, s') ∈ exec_event a"
assume a8:"(t, t') ∈ exec_event a"
have "s'∼d∼t'"
proof - {
have b1: "s' = s" using exec_event_def p1 a7
by simp
have b2: "t' = t" using exec_event_def p1 a8
by simp
have b3: "current s = current t" using domain_of_event_def a4
by simp
show ?thesis using a3 b1 b2
by blast
}
qed
}
then show ?thesis
using get_exec_prime_def
by (smt (verit, best) Pair_inject)
qed
lemma TEE_CheckMemoryAccessRights_weak_confidentiality_e:
"weak_confidentiality_e (hyperc (TEE_CHECKMEMORYACCESSRIGHTS aF memblock buffer_size))"
using TEE_CheckMemoryAccessRights_weak_confidentiality weak_confidentiality_e_def
by (smt (verit, del_insts) get_exec_prime_def)
lemma TEE_Malloc_weak_confidentiality:
assumes p1: "a = hyperc (TEE_MALLOC buffer_size h)"
shows "∀ d s t.
reachable0 s ∧
reachable0 t ∧
(s ∼ d ∼ t) ∧
((domain_of_event s a) = (domain_of_event t a)) ∧
(get_exec_prime s=get_exec_prime t)∧
((the (domain_of_event s a)) ↝ d) ∧
(s ∼ (the (domain_of_event s a)) ∼ t) ⟶
(∀ s' t'. (s, s') ∈ exec_event a ∧ (t, t') ∈ exec_event a ⟶ (s' ∼ d ∼ t'))"
proof -{
fix s t d s' t'
assume a1:"reachable0 s"
assume a2:"reachable0 t"
assume a3:"s∼d∼t"
assume a31:"exec_prime s=exec_prime t"
assume a4:"(domain_of_event s a) = (domain_of_event t a)"
assume a5:"(the (domain_of_event s a)) ↝ d"
assume a6:"s ∼ (the (domain_of_event s a)) ∼ t"
assume a7:"(s, s') ∈ exec_event a"
assume a8:"(t, t') ∈ exec_event a"
assume a9:"ta_mgr(TEE_state s) = ta_mgr(TEE_state t)"
assume a10:"TAs_state s = TAs_state t"
have "s'∼d∼t'"
proof - {
have b1: "s' = (TEE_Malloc sysconf s buffer_size h)" using exec_event_def p1 a7
by simp
have b2: "t' = (TEE_Malloc sysconf t buffer_size h)" using exec_event_def p1 a8
by simp
have b3: "current s = current t" using domain_of_event_def a4
by simp
show ?thesis
proof (cases "current s = TEE sysconf ∨ current s = REE sysconf")
case True
then show ?thesis using TEE_Malloc_def b1 b2 b3 a3
by metis
next
case False
have currents: "is_TA sysconf (current s)" using False
by auto
then show ?thesis
proof (cases "(exec_prime s) ≠ []")
case True
then show ?thesis using TEE_Malloc_def b1 b2 b3 a3 a31
by metis
next
case False
have h: "¬((exec_prime s) ≠ [])" using False
by simp
then show ?thesis
proof (cases "(h ≠ TEE_MALLOC_FILL_ZERO) ∧ (h ≠ TEE_USER_MEM_HINT_NO_FILL_ZERO)")
case True
then show ?thesis using TEE_Malloc_def b1 b2 b3 a3
by metis
next
case False
then have hh: "¬((h ≠ TEE_MALLOC_FILL_ZERO) ∧ (h ≠ TEE_USER_MEM_HINT_NO_FILL_ZERO))"
by simp
then show ?thesis
proof (cases "d = TEE sysconf")
case True
then have "(the (domain_of_event s a)) ∖↝ d" using interference1_def non_interference1_def currents
by auto
then show ?thesis using a5
by simp
next
case False
then show ?thesis
proof (cases "d = REE sysconf")
case True
then have "(the (domain_of_event s a)) ∖↝ d" using interference1_def non_interference1_def currents
by auto
then show ?thesis using a5
by simp
next
case False
then have g: "d ≠ REE sysconf"
by simp
then show ?thesis
proof (cases "d = TEE sysconf")
case True
then have "(the (domain_of_event s a)) ∖↝ d" using interference1_def non_interference1_def currents
by auto
then show ?thesis using a5
by simp
next
case False
then have gg: "d ≠ TEE sysconf"
by simp
then show ?thesis
proof (cases "is_TA sysconf d")
case True
then have f: "vpeq_TA s d t" using True vpeq1_def a3
by simp
have f1: "{x. x∈set(tee_memories (TEE_state s))∧ (ownership x=d)} =
{x. x∈set(tee_memories (TEE_state t))∧ (ownership x=d)}" using f
by simp
then show ?thesis
proof (cases "current s = d")
case True
then have td: "current t = d" using b3
by simp
let ?newTEESize = "tee_total_size(TEE_state s) - buffer_size"
let ?newblk = "mem_alloc s buffer_size"
let ?lst = "?newblk # tee_memories(TEE_state s)"
let ?newBIDpointer = "BIDpointer(ta_mgr(TEE_state s)) + 1"
have s's: "s' = s⦇TEE_state := (TEE_state s)⦇tee_total_size := ?newTEESize, tee_memories := ?lst, ta_mgr:=ta_mgr(TEE_state s)⦇BIDpointer:=?newBIDpointer⦈⦈⦈"
using TEE_Malloc_def b1 currents h hh mem_alloc_def False
by auto
let ?newTEESize_t = "tee_total_size(TEE_state t) - buffer_size"
let ?newblk_t = "mem_alloc t buffer_size"
let ?lst_t = "?newblk_t # tee_memories(TEE_state t)"
let ?newBIDpointer_t = "BIDpointer(ta_mgr(TEE_state t)) + 1"
have t't: "t' = t⦇TEE_state := (TEE_state t)⦇tee_total_size := ?newTEESize_t, tee_memories := ?lst_t, ta_mgr:=ta_mgr(TEE_state t)⦇BIDpointer:=?newBIDpointer_t⦈⦈⦈"
using TEE_Malloc_def b2 b3 currents mem_alloc_def False a31 h hh
by auto
have owneq: "ownership(?newblk) = ownership(?newblk_t)" using td b3 mem_alloc_def
by simp
have "{x. x∈set(tee_memories (TEE_state s'))∧ (ownership x=d)} =
{x. x∈set(tee_memories (TEE_state t'))∧ (ownership x=d)}"
proof - {
have b5: "block_id(?newblk) = block_id(?newblk_t)" using td b3 mem_alloc_def newMemBlockID3_def a9
by simp
have schange: "{x. x∈set(?newblk#tee_memories (TEE_state s)) ∧ (ownership x=d)} =
{x. x∈set(tee_memories (TEE_state s')) ∧ (ownership x=d)}"
using s's
by simp
have tchange: "{x. x∈set(?newblk_t#tee_memories (TEE_state t)) ∧ (ownership x=d)} =
{x. x∈set(tee_memories (TEE_state t')) ∧ (ownership x=d)}"
using t't
by simp
then show ?thesis using schange tchange owneq f1 mem_alloc_def b5
by auto
}
qed
then show ?thesis using vpeq1_def vpeq_TA_def g gg
by simp
next
case False
then have "(the (domain_of_event s a)) ∖↝ d" using non_interference1_def interference1_def currents
by auto
then show ?thesis using a5
by simp
qed
next
case False
then have ggg: "¬(is_TA sysconf d)"
by simp
then show ?thesis using g gg ggg
by simp
qed
qed
qed
qed
qed
qed
qed
}
qed
}
then show ?thesis
using get_exec_prime_def
by (smt (verit, best) Pair_inject)
qed
lemma TEE_Malloc_weak_confidentiality_e:
"weak_confidentiality_e (hyperc (TEE_MALLOC buffer_size h))"
using TEE_Malloc_weak_confidentiality weak_confidentiality_e_def
by (smt (verit, del_insts) get_exec_prime_def)
lemma TEE_Realloc_weak_confidentiality:
assumes p1: "a = hyperc (TEE_REALLOC memblock new_size)"
shows "∀ d s t.
reachable0 s ∧
reachable0 t ∧
(s ∼ d ∼ t) ∧
((domain_of_event s a) = (domain_of_event t a)) ∧
(get_exec_prime s=get_exec_prime t)∧
((the (domain_of_event s a)) ↝ d) ∧
(s ∼ (the (domain_of_event s a)) ∼ t) ⟶
(∀ s' t'. (s, s') ∈ exec_event a ∧ (t, t') ∈ exec_event a ⟶ (s' ∼ d ∼ t'))"
proof -{
fix s t d s' t'
assume a1:"reachable0 s"
assume a2:"reachable0 t"
assume a3:"s∼d∼t"
assume a31:"exec_prime s=exec_prime t"
assume a4:"(domain_of_event s a) = (domain_of_event t a)"
assume a5:"(the (domain_of_event s a)) ↝ d"
assume a6:"s ∼ (the (domain_of_event s a)) ∼ t"
assume a7:"(s, s') ∈ exec_event a"
assume a8:"(t, t') ∈ exec_event a"
have "s'∼d∼t'"
proof - {
have b1: "s' = (TEE_Realloc sysconf s memblock new_size)" using exec_event_def p1 a7
by simp
have b2: "t' = (TEE_Realloc sysconf t memblock new_size)" using exec_event_def p1 a8
by simp
have b3: "current s = current t" using domain_of_event_def a4
by simp
show ?thesis
proof (cases "current s = TEE sysconf ∨ current s = REE sysconf")
case True
then show ?thesis using TEE_Realloc_def b1 b2 b3 a3
by metis
next
case False
then have currents: "is_TA sysconf (current s)"
by auto
then show ?thesis
proof (cases "(exec_prime s) ≠ []")
case True
then show ?thesis using TEE_Realloc_def b1 b2 b3 a3 currents a31
by metis
next
case False
then have exec: "¬((exec_prime s) ≠ [])"
by simp
then show ?thesis
proof (cases "d = TEE sysconf")
case True
then have "(the (domain_of_event s a)) ∖↝ d" using non_interference1_def interference1_def currents
by auto
then show ?thesis using a5
by simp
next
case False
then have g: "d ≠ TEE sysconf"
by simp
then show ?thesis
proof (cases "d = REE sysconf")
case True
then have "(the (domain_of_event s a)) ∖↝ d" using non_interference1_def interference1_def currents
by auto
then show ?thesis using a5
by simp
next
case False
then have gg: "d ≠ REE sysconf"
by simp
then show ?thesis
proof (cases "is_TA sysconf d")
case True
then show ?thesis
proof (cases "current s = d")
case True
let ?newTEESize = "tee_total_size(TEE_state s) - new_size + (size memblock)"
let ?newTEESize_t = "tee_total_size(TEE_state t) - new_size + (size memblock)"
have s's: "s' = s⦇TEE_state := (TEE_state s)⦇tee_total_size := ?newTEESize⦈⦈" using TEE_Realloc_def currents exec b1 g gg True
by auto
have t't: "t' = t⦇TEE_state := (TEE_state t)⦇tee_total_size := ?newTEESize_t⦈⦈"
using TEE_Realloc_def currents b3 exec a31 b2 g gg True a3
by simp
have "vpeq_TA s d t ≡ {x. x∈set(tee_memories (TEE_state s))∧ (ownership x=d)} =
{x. x∈set(tee_memories (TEE_state t))∧ (ownership x=d)} "
using vpeq1_def vpeq_TA_def a3
by simp
then show ?thesis using s's t't currents True vpeq1_def vpeq_TA_def a3
by auto
next
case False
then have "(the (domain_of_event s a)) ∖↝ d" using non_interference1_def interference1_def currents
by auto
then show ?thesis using a5
by simp
qed
next
case False
then have ggg: "¬(is_TA sysconf d)"
by simp
then show ?thesis using g gg ggg
by simp
qed
qed
qed
qed
qed
}
qed
}
then show ?thesis
using get_exec_prime_def
by (smt (verit, best) Pair_inject)
qed
lemma TEE_Realloc_weak_confidentiality_e:
"weak_confidentiality_e (hyperc (TEE_REALLOC memblock new_size))"
using TEE_Realloc_weak_confidentiality weak_confidentiality_e_def
by (smt (verit, del_insts) get_exec_prime_def)
lemma TEE_Free_weak_confidentiality:
assumes p1: "a = hyperc (TEE_FREE memblock)"
shows "∀ d s t.
reachable0 s ∧
reachable0 t ∧
(s ∼ d ∼ t) ∧
((domain_of_event s a) = (domain_of_event t a)) ∧
(get_exec_prime s=get_exec_prime t)∧
((the (domain_of_event s a)) ↝ d) ∧
(s ∼ (the (domain_of_event s a)) ∼ t) ⟶
(∀ s' t'. (s, s') ∈ exec_event a ∧ (t, t') ∈ exec_event a ⟶ (s' ∼ d ∼ t'))"
proof -{
fix s t d s' t'
assume a1:"reachable0 s"
assume a2:"reachable0 t"
assume a3:"s∼d∼t"
assume a31:"exec_prime s=exec_prime t"
assume a4:"(domain_of_event s a) = (domain_of_event t a)"
assume a5:"(the (domain_of_event s a)) ↝ d"
assume a6:"s ∼ (the (domain_of_event s a)) ∼ t"
assume a7:"(s, s') ∈ exec_event a"
assume a8:"(t, t') ∈ exec_event a"
have "s'∼d∼t'"
proof - {
have b1: "s' = (TEE_Free sysconf s memblock)" using exec_event_def p1 a7
by simp
have b2: "t' = (TEE_Free sysconf t memblock)" using exec_event_def p1 a8
by simp
have b3: "current s = current t" using domain_of_event_def a4
by simp
show ?thesis
proof (cases "current s = TEE sysconf ∨ current s = REE sysconf")
case True
then show ?thesis using TEE_Free_def b1 b2 b3 a3
by metis
next
case False
then have currents: "is_TA sysconf (current s)"
by auto
then show ?thesis
proof (cases "(exec_prime s) ≠ [] ∨ ownership memblock ≠ current s")
case True
then show ?thesis using TEE_Free_def b1 b2 b3 a3 currents a31
by metis
next
case False
then have exec: "¬((exec_prime s) ≠ [] ∨ ownership memblock ≠ current s)"
by simp
then show ?thesis
proof (cases "d = TEE sysconf")
case True
then have "(the (domain_of_event s a)) ∖↝ d" using non_interference1_def interference1_def currents
by auto
then show ?thesis using a5
by simp
next
case False
then have g: "d ≠ TEE sysconf"
by simp
then show ?thesis
proof (cases "d = REE sysconf")
case True
then have "(the (domain_of_event s a)) ∖↝ d" using non_interference1_def interference1_def currents
by auto
then show ?thesis using a5
by simp
next
case False
then have gg: "d ≠ REE sysconf"
by simp
then show ?thesis
proof (cases "is_TA sysconf d")
case True
then show ?thesis
proof (cases "current s = d")
case True
then have sd: "current s = d"
by blast
then show ?thesis
proof (cases "memblock ∉ set(filter (λx.(ownership x) = (ownership memblock)) (tee_memories(TEE_state s)))")
case True
then have "memblock ∉ set(filter (λx.(ownership x) = (ownership memblock)) (tee_memories(TEE_state t)))"
using a6 vpeq1_def vpeq_TA_def sd exec g gg
by fastforce
then show ?thesis using TEE_Free_def b1 b2 b3 a3 currents a31 True
by metis
next
case False
then have subf: "¬(memblock ∉ set(filter (λx.(ownership x) = (ownership memblock)) (tee_memories(TEE_state s))))"
by blast
then have false1: "¬(memblock ∉ set(filter (λx.(ownership x) = (ownership memblock)) (tee_memories(TEE_state t))))"
using a6 vpeq1_def vpeq_TA_def sd exec g gg
by fastforce
show ?thesis
proof (cases "block_id memblock < 2")
case True
then show ?thesis using TEE_Free_def b1 b2 b3 a3 currents a31
by metis
next
case False
let ?newTEESize = "tee_total_size(TEE_state s) + (size memblock)"
let ?newlst = "filter (λx.(block_id x) ≠ (block_id memblock)) (tee_memories(TEE_state s))"
let ?newTEESize_t = "tee_total_size(TEE_state t) + (size memblock)"
let ?newlst_t = "filter (λx.(block_id x) ≠ (block_id memblock)) (tee_memories(TEE_state t))"
have s's: "s' = s⦇TEE_state := (TEE_state s)⦇tee_total_size := ?newTEESize, tee_memories := ?newlst⦈⦈"
using TEE_Free_def b1 currents exec False subf
by auto
have t't: "t' = t⦇TEE_state := (TEE_state t)⦇tee_total_size := ?newTEESize_t, tee_memories := ?newlst_t⦈⦈"
using TEE_Free_def b2 currents b3 exec a31 False false1
by auto
then show ?thesis using a3 s's t't
by auto
qed
qed
next
case False
then have "(the (domain_of_event s a)) ∖↝ d"
using non_interference1_def interference1_def currents
by auto
then show ?thesis using a5
by simp
qed
next
case False
then have ggg: "¬(is_TA sysconf d)"
by simp
then show ?thesis using g gg ggg
by simp
qed
qed
qed
qed
qed
}
qed
}
then show ?thesis
using get_exec_prime_def
by (smt (verit, best) Pair_inject)
qed
lemma TEE_Free_weak_confidentiality_e:
"weak_confidentiality_e (hyperc (TEE_FREE memblock))"
using TEE_Free_weak_confidentiality weak_confidentiality_e_def
by (smt (verit, del_insts) get_exec_prime_def)
end